#! /usr/bin/env python

import sys, re, string
from pycparser import c_parser, c_ast, parse_file
from tos2cprover_preprocess import *
from tos2cprover_parse import *
from tos2cprover_reach import *

if len(sys.argv) < 2:
  print "Usage: ./tos2cprover [file].c"
  sys.exit("Missing input, exiting.")

filein_name       = sys.argv[1]
filepp_name       = "outpp.c"
fileout_name      = "outaf.c"
fileoutrf_name    = "outrf.c"
#fileoutrfdup_name = "outrfdup.c"

filein        = open(filein_name,    'r')
filepp        = open(filepp_name,    'w+')
fileout       = open(fileout_name,   'w+')
fileoutrf     = open(fileoutrf_name, 'w+')
#fileoutrfdup  = open(fileoutrfdup_name, 'w+')

# Preprocess file
line = filein.readline()

while line != '':
  l1 = turn_dll_into__(line)
  l2 = remove_line_directives(l1)
  l3 = simplify_attr(l2)
  l4 = turn_asm_line_into_c(l3)
  filepp.write(l4)
  line = filein.readline()

filein.close()
filepp.close()

print 'Preprocessed file pp.c written'

# Parse file, after first
# having the preprocessor lines #... solved by cpp
ast = parse_file(filepp_name, use_cpp=True)
if not isinstance(ast, c_ast.FileAST):
  sys.exit("Incorrect AST")

print 'File parsed into AST'

print "-" * 80
# ast.show(attrnames=True, showcoord=False)
# print "-" * 80

# Compute dead function names
dead_func, common_func, sigs = deadfn(ast)
print '\nDead functions (%s):' %(len(dead_func))
print dead_func
#print '\nCommon functions (%s):' %(len(common_func))
#print common_func
print "-" * 80

# Compute commonly reachable data
common_data = comdata(ast)
print '\nCommon data (%s):' %(len(common_data))
print common_data

print "-" * 80

#--------------------------------------------------
# Write back the translated code into fileout
if __name__ == '__main__':

  libs = '''#include "lib/msp430_hw.h"
#include "lib/libc_string.h"

extern nondet_bv();

'''
  fileout.write(libs)
  c = code(ast)[0]
  fileout.write(c)
  fileout.close()

  fileoutrf.write(libs)
  d = code(ast, \
    include_deadfn=False, 
    deadfn_set=dead_func, 
    common_data=common_data,
    sig_func=sigs)[0]
  fileoutrf.write(d)
  fileoutrf.close()

#  fileoutrfdup.write(libs)
#  d = code(ast, \
#    include_deadfn=False, 
#    deadfn_set=dead_func, 
#    common_data=common_data,
#    common_func=common_func)[0]
#  fileoutrfdup.write(d)
#  fileoutrfdup.close()

  print "-" * 80

